<?php
$line = intval(isset($_GET['line']) ? $_GET['line'] : 100);
// Read grader log
?>
<h2>Grader log</h2>
Last <?php echo $line?> lines:<br />

<span style="font-family:courier,monospace">

<ol><li>
<?php
if (file_exists(GRADER_LOG)) {
$file = file(GRADER_LOG);
for ($l = count($file); $l > $line; $l--, array_shift($file));
$loop = new Loop('',' style="color:green"');
foreach ($file as $k=>$v) {
	$a = '<span' . (string)$loop . '>' . $v . '</span>';
	if (stristr($v, 'error')) $a = '<span style="color:red">' . $v . '</span>';
	$file[$k] = $a;
}
echo implode("</li>\n<li>", $file);
} else echo 'No log file found.';
?>
</li></ol>
</span>
